a, b, c:. 0 < c  (a  b  c * a  c * b) 

latex

Definitions	A, True, T, {T}, P & Q, t  T, , P  Q, P  Q, P  Q, P  Q, x:A. B(x), b, (i = j), ff, i <z j, tt, r + s, r - s, qpositive(r), p q, q_le(r;s), <+>, t.1, , gset, goset, t.2, , x f y, p  q, a < b, if b then t else f fi , a <p b, a < b, False, qeq(r;s), b, r * s, r < s, S  T
Lemmas	qmul one qrng, qmul inv, qmul comm qrng, qmul assoc qrng, qinv wf, assert-qeq, qeq wf2, assert wf, not functionality wrt iff, rationals wf, int inc rationals, true wf, squash wf, qmul preserves qless, qle-iff, qmul wf, qless wf, qle wf, iff functionality wrt iff